COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% Axioms for the abstract syntax of conditional expressions%
C00004 ENDMK
C⊗;
% Axioms for the abstract syntax of conditional expressions%

declare INDVAR e e1 e2 e3, INDCONST T F U, PREDCONST iscond 1 isprop 1,
	OPCONST mkcond 3 s1 1 s2 1 s3 1 value 1;

axiom	condsyn:
	∀e1 e2 e3. (isprop(e1) ⊃ iscond(mkcond(e1,e2,e3))),
	∀e1 e2 e3. s1(mkcond(e1,e2,e3)) = e1,
	∀e1 e2 e3. s2(mkcond(e1,e2,e3)) = e2,
	∀e1 e2 e3. s3(mkcond(e1,e2,e3)) = e3,
	∀e. (iscond(e) ⊃ (e = mkcond(s1(e),s2(e),s3(e)))),
	∀e1 e2 e3. (isprop(e1)∧isprop(e2)∧isprop(e3) ⊃ isprop(mkcond(e1,e2,e3)));

	condval:
	∀e. (iscond(e) ∧ value(s1(e)) = T ⊃ value(e) = value(s2(e))),
	∀e. (iscond(e) ∧ value(s1(e)) = F ⊃ value(e) = value(s3(e))),
	∀e. (iscond(e) ∧ value(s1(e)) = U ⊃ value(e) = U);

	condtri:
	∀e. (iscond(e) ⊃ isprop(s1(e))),
	∀e. (isprop(e) ⊃ value(e) = T ∨ value(e) = F ∨ value(e) = U);;